p:FinProbSpace, f:(), X:(n:RandomVariable(p;f(n))), n:.
(n:, i:{0..n}. f(i) < f(n))  (rv-partial-sum(n;i.X(i))  RandomVariable(p;f(n))) 

latex

Definitions

t  T, x:A. B(x), Outcome, , {x:A| B(x)} , x:AB(x), f(a), x(s), #$n, {i..j}, Type, FinProbSpace, a < b, A  B, x:A  B(x), P & Q, i  j < k, , Top, type List, P  Q, False, A, ||as||, Void, <a, b>, s = t, True, T, S  T, suptype(S; T), , , , A  B, x,y:A//B(x;y), if b then t else f fi , EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), , x,y. t(x;y), x. t(x), a  j < b. E(j), x.A(x), RandomVariable(p;n), rv-partial-sum(n;i.X(i))

Lemmas

random-variable wf, finite-prob-space wf, qsum wf, int-rational, quotient wf, bool wf, qeq wf2, btrue wf, b-union wf, int nzero wf, rationals wf, subtype rel function, squash wf, true wf, int seg properties, length wf nat, le wf, int seg wf, nat wf, p-outcome wf